*****ASSUME A(RW,w,W2,1)∧color(W2,w)=B;

1 A(RW,w,W2,1)∧color(W2,w)=B  (1)

*****∀E w12 RW,w,1;

2 (A(RW,w,W1,1)∨A(RW,w,W2,1))⊃A(RW,w,W12,1)  

*****∀E elweka1 w;

3 A(RW,w,W12,1)≡(A(RW,w,W12,0)∧∀p.(∀w1.(A(w,w1,p,0)⊃color(p,w1)=color(p,w))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(%
p,RW))))  

*****TAUT A(RW,w,W12,0) 1:3;

4 A(RW,w,W12,0)  (1)

*****TAUT ∀p.(∀w1.(A(w,w1,p,0)⊃color(p,w1)=color(p,w))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW))) 1:3;

5 ∀p.(∀w1.(A(w,w1,p,0)⊃color(p,w1)=color(p,w))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW)))  (1)

*****∀E ↑ W1;

6 ∀w1.(A(w,w1,W1,0)⊃color(W1,w1)=color(W1,w))≡∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW))  (1)